2-SAT问题

简单来说,2SAT2-SAT问题就是有nnboolbool变量,并给出了mm个限制关系,每个限制关系说的就是:如果xx取了某个值,则yy必须取某个值。形式化的语言就是:给定一个布尔式(xaxc)(xa¬xb)(xc¬xa)....(x_a\lor x_c)\land(x_a\lor \lnot x_b)\land (x_c\lor \lnot x_a)....问是否存在一组xx的取值方式,使得整个表达式可以为真。也可以要求输出一个具体方案。

2SAT2-SAT问题转换到图论上就是找一条可行性路径,想要做这个转换的话先要做点处理:因为对每个xx来说都有两种可能的取值,所以第一步先拆点,把每个值按真假拆成两个点。例如,对于点aia_i来说,他会被拆成ai,pa_{i,p}ai,qa_{i,q}(其中p,q{0,1}p,q\in \{0,1\}。把ai,0a_{i,0}建在ii,另外一个建在i+Ni+N即可。

2SAT2-SAT问题里,如果某个条件是:若aia_ipp的话,aja_j必须是qq,则在图中对i+pNi + p * Nj+qNj +q * N点连一条有向边。这个条件是蕴含了逆反命题的,即如果aia_i1p1-p的话,aja_j必须是1q1-q,假如说题目里没有明确指出所有条件的逆反命题都一定给出了,否则也要加入条件里。
这样处理之后我们就得到了一张有向图,由于条件具有传递性,并且图中可能有环,所以先进行SCC缩点。假如说已经SCCSCC缩点结束了:对于某个点ii来说,如果iii+Ni+N都在一个SCCSCC分量里,就出现了矛盾,说明问题无解,反之说明问题是有解的。
总体复杂度里只有求SCCSCC,因此是O(N+M)O(N+M)的。

现在就能判断说整个2SAT2-SAT问题是否是有解的了,那么怎么去输出一组可行解呢?既然说之前已经有了SCCSCC缩点过程了,联系一下SCCSCC的特性,可以想到使用stackstackSCCSCC缩点是有一个性质的:即最后可以得到一个缩完点之后的图的拓扑排序的逆序,只要再颠倒一次就可以得到一个拓扑排序了。得到拓扑排序之后,就可以知道关系之间的传递性了,这里可以猜测一下:如果给某个拓扑序较前的点赋某个值,那么他的¬i\lnot i关系就确定了(因为如果是相同的,就在一个SCCSCC里了,这里必须是不同的)。可以发现这样就可以确定所有的关系了:对于一个变量ii来说,如果他的拓扑序比¬i\lnot i更早,就把他设置成假,另外一个设置成真。

[HDU 3062] Party
原题链接:HDU 3062 Party
题目大意:有nn对夫妻被邀请参加聚会,每对夫妻只能来一个人.并且给定mm条矛盾关系,矛盾关系下两个人不能同时出现.问是否能恰好来nn个人

数据范围:
多组测试数据
1n10001 \leq n \leq 1000
1m<(n1)(n1)1 \leq m < (n - 1) * (n - 1)

把每对夫妻看成一个点,选择女方的时候取00,选男方的时候取11.当没有任何一对点在同一个SCCSCC里出现的时候,说明每对夫妻都出来了一个人,答案自然就是nn个人.所以直接判断是否有一对aaa+na+n出现在同一个SCCSCC即可.
考虑建图:

for(int i = 1;i <= m;++i)
{
    int a1,a2,c1,c2;scanf("%d%d%d%d",&a1,&a2,&c1,&c2);
    ++a1,++a2;
    if(c1 == 0)
    {
        if(c2 == 0)	add(a1,a2 + n),add(a2,a1 + n);
        else add(a1,a2),add(a2 + n,a1 + n);
    }
    else 
    {
        if(c2 == 0)	add(a1 + n,a2 + n),add(a2,a1);
        else add(a1 + n,a2),add(a2 + n,a1);
    }
}

这题直接分情况讨论就可以了,由于简单就不说太详细:
第一种是c1=0c1=0,c2=0c2=0,这种情况下表示a1a_1标号的女和a2a_2标号的女有矛盾,这个时候有两种情况:①是a1a_1女如果被选了,则a2a_2里只能选男,连(a1,a2+n)(a_1,a_2+n).第②种情况是a2a_2女被选了,此时a1a_1里只能选a1a_1男,连(a2,a1+n)(a_2,a_1 + n).其余情况分别讨论即可.

代码:

#define _CRT_SECURE_NO_WARNINGS
#include <vector>
#include <algorithm>
#include <cstdio>
#include <cstring>
#include <cmath>
#include <iostream>
#include <queue>
#include <set>
#include <map>
using namespace std;
typedef long long ll;
const int N = 4005,M = 4e6+7;
int edge[M],succ[M],ver[N],idx;
int time_stamp,dfn[N],low[N];
int n,m;
int stk[N],top;
bool in_stk[N];
int id[N],scc_cnt;
void add(int u,int v)
{
	edge[idx] = v;
	succ[idx] = ver[u];
	ver[u] = idx++;
}
void tarjan(int u)
{
	dfn[u] = low[u] = ++time_stamp;
	stk[++top] = u,in_stk[u] = 1;
	for(int i = ver[u];~i;i = succ[i])
	{
		int j = edge[i];
		if(!dfn[j])
		{
			tarjan(j);
			low[u] = min(low[u],low[j]);
		}
		else if(in_stk[j])	
			low[u] = min(low[u],dfn[j]);
	}
	if(dfn[u] == low[u])
	{
		int y;
		++scc_cnt;
		do
		{
			y = stk[top--];
			in_stk[y] = 0;
			id[y] = scc_cnt;
		}while(y != u);
	}
}

int main()
{
	while(scanf("%d%d",&n,&m) == 2)
	{
		memset(ver,-1,sizeof ver);
		memset(dfn,0,sizeof dfn);
		idx = 0;top = 0;time_stamp = 0;scc_cnt = 0;
		memset(in_stk,0,sizeof in_stk);
		memset(low,0,sizeof low);
		for(int i = 1;i <= m;++i)
		{
			int a1,a2,c1,c2;scanf("%d%d%d%d",&a1,&a2,&c1,&c2);
			++a1,++a2;
			if(c1 == 0)
			{
				if(c2 == 0)	add(a1,a2 + n),add(a2,a1 + n);
				else add(a1,a2),add(a2 + n,a1 + n);
			}
			else 
			{
				if(c2 == 0)	add(a1 + n,a2 + n),add(a2,a1);
				else add(a1 + n,a2),add(a2 + n,a1);
			}
		}
		for(int i = 1;i <= 2 * n;++i)
			if(!dfn[i])
				tarjan(i);
		int ok = 1;
		for(int i = 1;i <= n;++i)
			if(id[i] == id[i + n])
			{
				ok = 0;
				break;
			}
		if(!ok)	puts("NO");
	    else puts("YES");
	}
    return 0;
}

[POJ 3678] Katu puzzle
原题链接:POJ 3578 Katu puzzle
题目大意:给定nnboolbool变量,一共有mm个关系,每个关系按如下的方式给出:xopy=cx op y = c,其中opop可以有:andandororxorxor三种。其余数字均为0011。问是否存在一组取值,使所有条件都能满足。
数据范围:
1N1031 \leq N \leq 10^3
0M1060 \leq M \leq 10^6

首先比较明显的一点就是,这个题的形式很像是2SAT2-SAT问题,不过运算方面都是位运算,所以第一步明显是要做一个转换。按表达式的类型进行分类考虑即可:
aa表示xa=0x_a=0a+Na+N表示xa=1x_a=1
xa&xb=0x_a \And x_b = 0
xa=1x_a=1时,xbx_b只能取00,连a+Na+Nbb
xb=1x_b=1时,xax_a只能取00,连b+Nb+Naa
注意2SAT2-SAT描述的是必须关系,虽然说两个00也是满足表达式的,但是不是必须关系,只要有一边是00那么答案已经确定了。
xa&xb=1x_a \And x_b = 1
两者只能是同时为一,如果出现了让他选00的情况就直接矛盾。
xa=0x_a=0,则必须xa=1x_a = 1,连aaa+Na+N
xb=0x_b=0,则必须xb=1x_b= 1,连bbb+Nb+N
xaxb=0x_a | x_b = 0
a+Na+Naa,连b+Nb+Nbb
xaxb=1x_a | x_b = 1
aab+Nb+N,连bba+Na+N
xaxb=0x_a \oplus x_b = 0
aabb,a+Na+Nb+Nb+N以及两种对称情况.
xaxb=1x_a \oplus x_b = 1
aab+Nb+N,bba+Na+N以及两种对称情况.

这里解释一下为什么②情况下是aa连的a+Na+N,这看起来很不正常,因为判据就是aa不能和a+Na+N在一个SCCSCC之内.这里这样做的原因实际上是:这里不管怎样都必须选a=1a=1,在没有a=0a=0的条件下是不会出现两者在一个SCCSCC里的.也就是保证说aa一定是11的,不会有第二种情况.另外一个这样操作的也是同理.

连完边之后SCCSCC缩点,对每个点判断一下是不是存在说有aaa+Na+N是一个SCCSCC内即可.
代码:

#define _CRT_SECURE_NO_WARNINGS
#include <bits/stdc++.h>
using namespace std;
typedef long long ll;
const int N = 2005,M = 4e6+7;
int edge[M],succ[M],ver[N],idx;
int time_stamp,dfn[N],low[N];
int n,m;
int stk[N],top;
bool in_stk[N];
int id[N],scc_cnt,siz[N];
int din[N],dout[N];
void add(int u,int v)
{
	edge[idx] = v;
	succ[idx] = ver[u];
	ver[u] = idx++;
}
void tarjan(int u)
{
	dfn[u] = low[u] = ++time_stamp;
	stk[++top] = u,in_stk[u] = 1;
	for(int i = ver[u];~i;i = succ[i])
	{
		int j = edge[i];
		if(!dfn[j])
		{
			tarjan(j);
			low[u] = min(low[u],low[j]);
		}
		else if(in_stk[j])	
			low[u] = min(low[u],dfn[j]);
	}
	if(dfn[u] == low[u])
	{
		int y;
		++scc_cnt;
		do
		{
			y = stk[top--];
			in_stk[y] = 0;
			id[y] = scc_cnt;
			siz[scc_cnt]++;
		}while(y != u);
	}
}

int main()
{
	memset(ver,-1,sizeof ver);
	scanf("%d%d",&n,&m);
	char opt[5];
	while(m--)
	{
		int u,v,c;scanf("%d%d%d",&u,&v,&c);
		++u;++v;
		scanf("%s",opt);getchar();
		if(opt[0] == 'A')	
		{
			if(c == 0)	add(u + n,v),add(v + n,u);
			else add(u,u + n),add(v,v + n);
		}
		else if(opt[0] == 'O')
		{
			if(c == 0)	add(u + n,u),add(v + n,v);
			else add(u,v + n),add(v,u + n);
		}
		else 
		{
			if(c == 0)	add(u,v),add(v,u),add(u + n,v + n),add(v + n,u + n);
			else add(u,v + n),add(v + n,u),add(v,u + n),add(u + n,v);
		}
	}
	for(int i = 1;i <= n * 2;++i)
		if(!dfn[i])
			tarjan(i);
	int ok = 1;
	for(int i = 1;i <= n;++i)
		if(id[i] == id[i + n])
		{
			ok = 0;
			break;
		}
	if(!ok)	puts("NO");
	else puts("YES");
    return 0;
}

其余几个题写了单独的题解

POJ 3683 Priest John's Busiest Day
POJ 2723 Get Luffy Out